(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 1))
(let ((e3 3))
(let ((e4 (* v1 e3)))
(let ((e5 (/ e2 (- e3))))
(let ((e6 (/ e3 e2)))
(let ((e7 (* e6 e6)))
(let ((e8 (- v1)))
(let ((e9 (/ e2 e2)))
(let ((e10 (* e8 v1)))
(let ((e11 (+ e9 e10)))
(let ((e12 (/ e2 (- e2))))
(let ((e13 (- e4)))
(let ((e14 (- e10 e12)))
(let ((e15 (- e5)))
(let ((e16 (+ e13 e10)))
(let ((e17 (+ e13 e4)))
(let ((e18 (/ e2 e3)))
(let ((e19 (- v0 e5)))
(let ((e20 (distinct e13 e19)))
(let ((e21 (distinct e12 e5)))
(let ((e22 (>= e16 e12)))
(let ((e23 (>= e7 e4)))
(let ((e24 (= e17 e7)))
(let ((e25 (<= e15 e7)))
(let ((e26 (> e13 e18)))
(let ((e27 (= e6 e13)))
(let ((e28 (< e11 e11)))
(let ((e29 (< e16 e7)))
(let ((e30 (> e10 e5)))
(let ((e31 (<= e8 e9)))
(let ((e32 (< e17 e14)))
(let ((e33 (= e18 e6)))
(let ((e34 (distinct e14 e6)))
(let ((e35 (>= e11 e9)))
(let ((e36 (= e14 e9)))
(let ((e37 (> e6 e19)))
(let ((e38 (>= e13 e9)))
(let ((e39 (> e12 e5)))
(let ((e40 (< e11 e11)))
(let ((e41 (< e6 e10)))
(let ((e42 (< e11 e13)))
(let ((e43 (> e7 e19)))
(let ((e44 (> e4 e7)))
(let ((e45 (distinct e19 e8)))
(let ((e46 (distinct e13 e15)))
(let ((e47 (<= e13 e14)))
(let ((e48 (= e5 e8)))
(let ((e49 (distinct e14 e14)))
(let ((e50 (> e15 e7)))
(let ((e51 (distinct e5 e15)))
(let ((e52 (< v0 e8)))
(let ((e53 (>= e18 e4)))
(let ((e54 (= e11 e4)))
(let ((e55 (= e17 e6)))
(let ((e56 (= e10 e18)))
(let ((e57 (< e16 e13)))
(let ((e58 (>= e4 e8)))
(let ((e59 (<= e9 e18)))
(let ((e60 (distinct e8 e17)))
(let ((e61 (>= e6 e13)))
(let ((e62 (< e10 e14)))
(let ((e63 (distinct e13 e10)))
(let ((e64 (= e7 e12)))
(let ((e65 (distinct e7 v0)))
(let ((e66 (= e13 e13)))
(let ((e67 (>= e17 e4)))
(let ((e68 (<= e4 e11)))
(let ((e69 (= e13 e15)))
(let ((e70 (distinct v0 e18)))
(let ((e71 (>= e12 e14)))
(let ((e72 (< e14 e9)))
(let ((e73 (< e6 e12)))
(let ((e74 (< e4 v1)))
(let ((e75 (distinct e15 e11)))
(let ((e76 (distinct e8 e4)))
(let ((e77 (> e8 e14)))
(let ((e78 (>= e11 e19)))
(let ((e79 (< e17 v0)))
(let ((e80 (<= e16 e13)))
(let ((e81 (= e9 e6)))
(let ((e82 (= e11 e9)))
(let ((e83 (>= e17 e6)))
(let ((e84 (<= e8 e8)))
(let ((e85 (< e6 e5)))
(let ((e86 (> e18 e7)))
(let ((e87 (distinct e12 e4)))
(let ((e88 (< e5 e11)))
(let ((e89 (>= e18 e9)))
(let ((e90 (>= e7 e18)))
(let ((e91 (= e12 e4)))
(let ((e92 (< e19 e13)))
(let ((e93 (= e11 e18)))
(let ((e94 (distinct e19 v1)))
(let ((e95 (distinct e18 e9)))
(let ((e96 (<= e16 v0)))
(let ((e97 (>= e7 e10)))
(let ((e98 (ite e51 e26 e31)))
(let ((e99 (= e90 e83)))
(let ((e100 (= e72 e28)))
(let ((e101 (and e22 e89)))
(let ((e102 (and e39 e40)))
(let ((e103 (= e65 e54)))
(let ((e104 (=> e85 e66)))
(let ((e105 (xor e73 e80)))
(let ((e106 (and e96 e87)))
(let ((e107 (= e70 e43)))
(let ((e108 (and e60 e100)))
(let ((e109 (= e34 e68)))
(let ((e110 (xor e59 e88)))
(let ((e111 (xor e77 e71)))
(let ((e112 (xor e20 e101)))
(let ((e113 (xor e106 e99)))
(let ((e114 (ite e25 e44 e48)))
(let ((e115 (=> e62 e47)))
(let ((e116 (= e81 e91)))
(let ((e117 (ite e110 e94 e95)))
(let ((e118 (ite e38 e82 e113)))
(let ((e119 (and e55 e55)))
(let ((e120 (or e57 e21)))
(let ((e121 (not e116)))
(let ((e122 (ite e30 e29 e75)))
(let ((e123 (and e64 e114)))
(let ((e124 (=> e122 e67)))
(let ((e125 (or e107 e123)))
(let ((e126 (xor e117 e56)))
(let ((e127 (ite e93 e119 e111)))
(let ((e128 (and e61 e24)))
(let ((e129 (ite e50 e50 e53)))
(let ((e130 (and e76 e63)))
(let ((e131 (= e108 e102)))
(let ((e132 (and e131 e98)))
(let ((e133 (= e52 e36)))
(let ((e134 (xor e33 e121)))
(let ((e135 (= e46 e133)))
(let ((e136 (or e118 e104)))
(let ((e137 (=> e132 e132)))
(let ((e138 (ite e112 e32 e84)))
(let ((e139 (xor e86 e74)))
(let ((e140 (and e128 e135)))
(let ((e141 (= e23 e49)))
(let ((e142 (or e45 e92)))
(let ((e143 (= e127 e27)))
(let ((e144 (xor e143 e79)))
(let ((e145 (=> e69 e41)))
(let ((e146 (or e129 e136)))
(let ((e147 (= e144 e145)))
(let ((e148 (or e105 e134)))
(let ((e149 (xor e139 e140)))
(let ((e150 (xor e78 e109)))
(let ((e151 (not e37)))
(let ((e152 (xor e138 e125)))
(let ((e153 (not e42)))
(let ((e154 (ite e141 e151 e149)))
(let ((e155 (xor e103 e152)))
(let ((e156 (and e58 e150)))
(let ((e157 (ite e137 e142 e126)))
(let ((e158 (not e155)))
(let ((e159 (and e158 e115)))
(let ((e160 (= e153 e148)))
(let ((e161 (or e97 e147)))
(let ((e162 (= e161 e161)))
(let ((e163 (not e35)))
(let ((e164 (or e157 e162)))
(let ((e165 (ite e164 e160 e160)))
(let ((e166 (not e156)))
(let ((e167 (xor e130 e120)))
(let ((e168 (or e163 e165)))
(let ((e169 (xor e159 e159)))
(let ((e170 (= e169 e168)))
(let ((e171 (not e170)))
(let ((e172 (or e124 e166)))
(let ((e173 (ite e146 e154 e146)))
(let ((e174 (or e167 e173)))
(let ((e175 (ite e171 e171 e171)))
(let ((e176 (or e174 e175)))
(let ((e177 (and e172 e172)))
(let ((e178 (xor e176 e177)))
e178
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
